| Definitions | s = t, t  T, ES, AbsInterface(A), E(X), x:A  B(x), e c e',  x:A. B(x), <a, b>, Type, E, P   Q, x:A  B(x),  b, left + right, P  Q, (e < e'), {x:A| B(x)} , Top, f(a),  , prior-f-fixedpoints(e), (x l), let x,y = A in B(x;y), t.1, a:A fp B(a), strong-subtype(A;B), type List, EqDecider(T), Unit, IdLnk, Id, EOrderAxioms(E; pred?; info), EState(T), Knd,   x. t(x), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M),  ,  , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r s, constant_function(f;A;B), P & Q, loc(e), kind(e),  , S  T,  , Outcome, #$n, A B, a < b, ||as||, Void, False,  A, l[i], |g|, A c B, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi ,  x:A. B(x), e  X, [], {T}, n+m, n - m, SWellFounded(R(x;y)), pred!(e;e'), pred(e), first(e), i  j , -n, ff, e = e', f**(e), [car / cdr], prior(X), X(e), as @ bs, b, tt, P  Q, p q, p q, p q, i <z j, i z j, SQType(T), s ~ t, p =b q, (i = j), x =a y, null(as), a < b, x f y, a < b, [d], eq_atom$n(x;y), q_le(r;s), q_less(a;b), qeq(r;s), a = b, a = b, deq-member(eq;x;L), A List , sender(e), e loc e' , (e <loc e'), P Q |